es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} . e[e1,e2].False  (e2 <loc e1) 

latex

Definitions	x:A. B(x), P  Q, e[e1,e2].P(e), P & Q, P  Q, P  Q, t  T, , False, Dec(P), P  Q
Lemmas	es-le wf, false wf, es-locl wf, Id wf, es-loc wf, es-E wf, event system wf, decidable es-locl, es-le weakening eq, es-le-not-locl, es-locl transitivity2, es-locl irreflexivity